Nuprl Lemma : ma-empty_wf
11,40
postcript
pdf
MsgA
latex
Definitions
FinProbSpace
,
t
T
,
Id
,
x
.
A
(
x
)
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
,
IdLnk
,
type
List
,
Knd
,
x
:
A
B
(
x
)
,
Void
,
Type
,
Top
,
x
:
A
B
(
x
)
,
State(
ds
)
,
,
,
mk-ma
,
,
MsgA
Lemmas
mk-ma
wf
,
bool
wf
,
rationals
wf
,
ma-state
wf
,
top
wf
,
Knd
wf
,
Id
wf
,
IdLnk
wf
,
fpf-empty
wf
,
finite-prob-space
wf
origin
T, Id, 
x.A(x), 
x. t(x), 
x:A. B(x), 
, IdLnk, type List, Knd, x:A 
B(x), Void, Type, Top, x:A
B(x), State(ds), 
, 
, mk-ma, , MsgA